es:ES, A:Type, X:AbsInterface(A List), e:E.
(0 < ||es-interface-history(es;X;e)||)
 (e':E. (((e'  X)) & e' loc e  & (0 < ||X(e')||))) 

latex

Definitions

x:A  B(x), P & Q, x:A. B(x), a < b, s = t, t  T, x:AB(x), x:A. B(x), ES, EState(T), a:A fp B(a), f(a), Id, , strong-subtype(A;B), P  Q, Type, EqDecider(T), Unit, left + right, IdLnk, EOrderAxioms(E; pred?; info), kindcase(k; a.f(a); l,t.g(l;t) ), Knd, loc(e), kind(e), Msg(M), type List, , val-axiom(E;V;M;info;pred?;init;Trans;Choose;Send;val;time), r  s, e < e', , b, constant_function(f;A;B), SWellFounded(R(x;y)), , pred!(e;e'), x,y. t(x;y), Void, x:A.B(x), Top, S  T, suptype(S; T), first(e), A, <a, b>, pred(e), x.A(x), x. t(x), E, AbsInterface(A), let x,y = A in B(x;y), e  X, e loc e' , {x:A| B(x)} , E(X), t.1, case b of inl(x) => s(x) | inr(y) => t(y), if b then t else f fi , P  Q, (e <loc e'), X(e), ||as||, , A c B, i  j , #$n, P  Q, es-interface-history(es;X;e), Outcome, (x  l), P  Q, False, [], A  B, l[i], |g|

Lemmas

member-exists2, member-exists, select wf, l member wf, ge wf, member-es-interface-history, length of not nil, member exists, false wf, es-interface wf, iff wf, es-le weakening eq, es-interface-history wf, rev implies wf, es-le wf, length wf1, es-interface-val wf, es-interface-val wf2, es-E-interface wf, es-is-interface wf, es-E wf, deq wf, EOrderAxioms wf, kind wf, Msg wf, nat wf, val-axiom wf, cless wf, qle wf, bool wf, Knd wf, kindcase wf, IdLnk wf, constant function wf, loc wf, not wf, assert wf, first wf, top wf, unit wf, pred! wf, strongwellfounded wf, member wf, rationals wf, Id wf, EState wf, subtype rel wf, event system wf